Marginalia — Cuaderno Interactivo Marginalia Song Status Prospects Formal2023

> PUBLICACIÓNScience and Technology Foresight (2023)

REFERENCIA DOI

Serving as a foundation, cryptography is the key technique for ensuring network and information security. However, cryptographic implementations suffer from various security threats. Formal verification is the most important technique for rigorously proving the security of cryptographic implementations. This article first reviews the development status and application of formal verification techniques for cryptographic implementations both in China and abroad in terms of functional correctness, memory security, and side-channel security including time and power consumption. Then the article summarizes the drawbacks, current challenges, and development trends of these formal verification techniques for cryptographic implementations. According to the security requirements and limited progress in formal verification techniques for cryptographic implementations in China, it is suggested that high-performance and high-assurance cryptographic libraries should be constructed. In addition, the article proposes to follow the top-down design principle, strengthen independent innovation, and unify intermediate representation language under the guidance of national key task, and it plans to develop a high-efficiency, high-precision, and full-automated formal verification platform and a secure compiler optimization toolchain, create high-performance and high-assurance common cryptographic library with minimized trusted computing base, and promote the integrated development of both academic and industrial communities, so as to improve national network and information security. \copyright 2023 Science and Technology Review Publishing House. All rights reserved.

VER ABSTRACT

[ + ]

> NAVEGACIÓN

https://emanuel_quintana.codeberg.page/Marginalia/ LIVE

Índice General

Marginalia / Lecturas en curso LIVE

Índice de Leyendo

> REPOSITORIO

README.mdPREVIEW

Marginalia

Sitio en vivo: codeberg.page/Marginalia

Marginalia: notas escritas al margen de un libro.

Catálogo, notas, ensayos y código de lectura — economía, matemática, ciencias de la computación, literatura, física e ingeniería, y más.

Español

Este repositorio es mi cuaderno de lectura público, usando Org-mode y org-babel.

Licencias

Este repositorio usa doble licencia: código bajo MIT, notas y ensayos bajo CC BY-SA 4.0.

Ver en Codeberg

> LICENCIAS

LICENSEMIT PREVIEW

MIT License

Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files, to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED.

NOTE: Aplica solo al código fuente. El contenido escrito está bajo CC BY-SA 4.0.

Código — MIT

LICENSE-CONTENT.mdPREVIEW

Licencia de contenido

Este archivo cubre las notas de lectura, ensayos y textos en lecturas/ y ensayos/.

Creative Commons BY-SA 4.0

Sos libre de:

Compartir — copiar y redistribuir el material.
Adaptar — remezclar, transformar y construir a partir del material.

Bajo los siguientes términos: Atribución y ShareAlike.

CC BY-SA 4.0

Marginalia — Emanuel Quintana Silva Última actualización: 2026-07-22

Validate